'\" t
.\"     Title: cop man page
.\"    Author: bjarneh@ifi.uio.no
.\"      Date: May.25.2011
.\"    Manual: cop manual
.\"    Source: cop 0.2
.\"  Language: English
.\"      Misc: I took this man page from git, and modified it
.\"
.TH "cop" "1" "May/25/2011" "cop 0\&.2\&.0" "cop manual"
.\" -----------------------------------------------------------------
.\" * Define some portability stuff
.\" -----------------------------------------------------------------
.\" ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.\" http://bugs.debian.org/507673
.\" http://lists.gnu.org/archive/html/groff/2009-02/msg00013.html
.\" ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.ie \n(.g .ds Aq \(aq
.el       .ds Aq '
.\" -----------------------------------------------------------------
.\" * set default formatting
.\" -----------------------------------------------------------------
.\" disable hyphenation
.nh
.\" disable justification (adjust text to left margin only)
.ad l
.\" -----------------------------------------------------------------
.\" * MAIN CONTENT STARTS HERE *
.\" -----------------------------------------------------------------
.SH "NAME"
cop \- coherent theorem prover
.SH "SYNOPSIS"
.sp
.nf
cop [OPTIONS] input.gl
.fi
.sp
.SH "DESCRIPTION"
.sp
cop is a theorem prover for coherent logic, sometimes referred to as geometric logic. it implements a modified version of the RETE algorithm for its matching, and some modular strategies which can be turned on/off\&.
.sp
To see the complete manual:  http://cop\&.googlecode\&.com
.PP
.SH "OPTIONS"
.PP
.B
\-h, \-\-help
.RS 4
print legal options and exit
.RE
.PP
.B
\-v, \-\-version
.RS 4
print version and exit
.RE
.PP
.B
\-V, \-\-verbose
.RS 4
alias for \-\-loglevel=INFO
.RE
.PP
.B
\-a, \-\-accurate
.RS 4
display an accurate time (does not timeout)
.RE
.PP
.B
\-t, \-\-timeout
.RS 4
timeout in seconds for each strategy (default: 2)
.RE
.PP
.B
\-l, \-\-list
.RS 4
list system and config properties
.RE
.PP
.B
\-d, \-\-dot
.RS 4
create a dot\-file of proof tree (see manual graphviz/dot)
.RE
.PP
.B
\-m, \-\-maxpaths
.RS 4
max number of open paths before we give up (default: 1000)
.RE
.PP
.B
\-P, \-\-paths
.RS 4
print number of open paths during run
.RE
.PP
.B
\-r, \-\-recursive
.RS 4
recursively prove all files in directory tree
.RE
.PP
.B
\-s, \-\-strategy
.RS 4
choose strategy: simple, rete, hrete, main, all (default: main)
.RE
.PP
.B
\-o, \-\-order
.RS 4
match order: hash, time, random (default: hash)
.RE
.PP
.B
\-p, \-\-plain
.RS 4
no ANSI color codes are printed
.RE
.PP
.B
\-c, \-\-cmp
.RS 4
choose comparator see \-\-listcmp
.RE
.PP
.B
\-i, \-\-ignore
.RS 4
ignore fact\-set, i\&.e\&. allow re\-use of facts
.RE
.PP
.B
\-\-listcmp
.RS 4
list comparators and explanation
.RE
.PP
.B
\-\-single
.RS 4
match only one new fact in each round
.RE
.PP
.B
\-\-seed
.RS 4
for randomized strategies
.RE
.PP
.B
\-\-dotfmt
.RS 4
convert dot\-file to given format \fBnull\fR turns it off (default: eps)
.RE
.PP
.B
\-\-dotmax
.RS 4
max number of nodes in dot\-file
.RE
.PP
.B
\-\-dotheader
.RS 4
font\-size of header in dot\-file (default: 25)
.RE
.PP
.B
\-\-loglevel
.RS 4
DEBUG, INFO, WARNING(default), ERROR, FATAL
.RE
.PP
.B
\-\-ll
.RS 4
alias for \-\-loglevel
.RE
.PP
.B
\-\-logfile
.RS 4
write to logfile as well as stderr
.RE
.PP
.B
\-\-lf
.RS 4
alias for \-\-logfile
.RE
.PP
.B
\-\-hidden
.RS 4
include hidden files and directories when \-\-recursive
.RE
.PP
.RE
.SH "FORMAT"
.sp
in order to prove a theorem it must be represented in a format understandable to the prover naturally, and the format used by \fBcop\fR is taken from the \fBgeolog\fR prover by J\&. Fisher and M\&. Bezem\&. predicates start with a lowercase letter, variables with an uppercase letter\&. quantifiers are implicit, any variable occurring in the argument which also occurs in the conclusion is universally quantified\&. variables which only occur in the conclusion is existentially quantified\&.
.sp
.if n \{\
.RS 4
.\}
.nf
%
% A \*(Aq%\*(Aq character indicates a comment\&.
%

true => p(a), q(c,d)\&.        % variables not allowed in fact\-rules
true => a,d\&.                 % propositional fac\-rule
p(X) => q(X)\&.                % implicit universal quantifier for X
p(X,Y) => q(X,Y), r(X,Z)\&.    % implicit existential quantifier for Z
p(a,b) => false\&.             % goal\-rule can close branch
p(X) => q(X); r(Y)\&.          % disjunction inside conclusion (forks)
.fi
.if n \{\
.RE
.\}
.sp
for an input theory to be proven it must also represent a contradiction i\&.e\&. a negated theorem\&.
.sp
.RE
.SH "CONFIGURATION"
.sp
this program is a command line tool, i\&.e\&. learning a new syntax for configuration seems a bit over the top\&. configuration is basically handled by writing command line arguments into \fB$HOME/\&.coprc\fR\&.
.sp
.if n \{\
.RS 4
.\}
.nf
#
# A \*(Aq#\*(Aq character indicates a comment\&.
#

-dotfmt=null         # do not convert dot-graph to image 
-timeout=3           # timeout == 3 seconds for each strategy
-maxpaths=320        # allow at most 320 open paths before giving up

.fi
.if n \{\
.RE
.\}
.sp
.SH "EXAMPLES"
.sp
.B
cop input.gl -timeout 4
.RS 4
try to prove input formula in file \fBinput\&.gl\fR using \fBmain\fR strategies with a timeout set to 4 seconds for each strategy
.RE
.PP
.B
cop input.gl \-timeout 4 \-ignore
.RS 4
same as the first one, but \fBignore\fR the fact\-set, i\&.e\&. allow re\-use of facts
.RE
.PP
.B
cop \-\-recursive problem/ 
.RS 4
recursively try to prove all formulas, or input files in \fBproblem\fR directory
.RE
.PP
.B
cop \-strategy rete input\&.gl \-cmp main
.RS 4
try to prove the formula in input\&.gl using the \fBrete\fR strategy using the \fBmain\fR comparators
.RE
.PP
.B
cop \-strategy simple input\&.gl \-paths
.RS 4
try to prove the formula in input\&.gl using the \fBsimple\fR strategy and print number of open paths during proof\-search
.RE
.PP
.B
cop \-strategy hrete input\&.gl \-dotfile=graph\&.dot
.RS 4
try to prove the formula in input\&.gl using the \fBhrete\fR strategy and write proof\-tree to dot\-file graph\&.dot, and try to convert graph\&.dot into \fBeps\fR, i\&.e\&. also produce file graph\&.dot\&.eps containing postscript of the proof\-tree
.RE
.SH "BUGS"
.sp
who knows\&.
.SH "AUTHORS"
.sp
bjarneh@ifi.uio.no
.SH "DOCUMENTATION"
.sp
http://cop.googlecode.com
